表現不可能な関手の例: List
表現不可能なものの例 List
なぜListは無理なのか
List aは、リストに依って要素数が異なる
従って少なくとも、Integer -> aとは一対一対応できない
対応付けようと考えると以下のようになる
要素数が0のList aの場合
Void -> a
要素数が1の場合
() -> a
要素数が2の場合
Bool -> a
例えば以下のように対応付けられる
code:hs
f0_0 :: Bool -> Int -- 0,0と対応 f0_0 True = 0
f0_0 False = 0
f0_1 False = 1
f99_100 True = 99 -- 99,100と対応 f99_100 False = 100
..
これら(Void, (), Bool, ...)を統一的に表すような型Rep f :: *が必要になるが、そんなものはない
以下の2つが同型である、ということ
List a
b -> a
実際にindexを定義しようとするとどうなるか